Postée il y a 12 jours
La vérification informatique des preuves mathématiques fournit un moyen pour les mathématiciens de concevoir, sauvegarder et transmettre des développements de théories mathématiques complexes tout en gardant un niveau exigeant de rigueur. Cependant, l'utilisation de ces technologies est freinée par la difficulté de fournir l'ensemble important de détails nécessaires à une preuve entièrement formalisée. Multiples approches ont été proposées et sont sous considération.
Le cadre défini par le projet Malinca consiste, à partir d'un texte rédigé en langue naturelle, comportant des raisonnements textuels à la manière classique, d'annoter et d'organiser ces informations avec des couches successives de précisions, avant d'arriver à un niveau apte à être traduit en preuve formelles. Dans ce processus, il y a des nombreux problèmes de quête de solutions, par exemple le remplissage dans une preuve des petites étapes considérées comme évidentes par l'auteur, la recherche d'énoncés intermédiaires utiles dans une preuve plus longue, ou la recherche des définitions et de lemmes pertinents dans une base de données.
Le question pour la thèse sera de travailler sur la recherche computationelle de structures, de stratégies et d'informations dans le contexte d'un développement mathématique, afin d'améliorer le processus d'automatisation de la création de preuves formelles pour une question mathématique donnée.
Co-dirigée par David Alfaya (Comillas, Madrid) et co-encadrée par Hugo Herbelin (INRIA, Paris)